$\forall$$A$:Type\{i\}. discrete\_struct\{i:l\}($A$) $\in$ Type\{i'\}